Petar Vukmirovic
2020-05-29 14:54:0 (GMT)
After rewriting and beta-normalizing the problem becomes this:
image.png
Petar Vukmirovic
2020-05-29 14:54:51 (GMT)
Symbols are defined as (TPTP code follows):
Petar Vukmirovic
2020-05-29 14:55:11 (GMT)
thf(f0,type,(
f0: $o > $o )).
thf(f0f,axiom,
( ( f0 @ $false )
= $false )).
thf(f0t,axiom,
( ( f0 @ $true )
= $false )).
thf(f1,type,(
f1: $o > $o )).
thf(f1f,axiom,
( ( f1 @ $false )
= $true )).
thf(f1t,axiom,
( ( f1 @ $true )
= $false )).
thf(f2,type,(
f2: $o > $o )).
thf(f2f,axiom,
( ( f2 @ $false )
= $false )).
thf(f2t,axiom,
( ( f2 @ $true )
= $true )).
thf(f3,type,(
f3: $o > $o )).
thf(f3f,axiom,
( ( f3 @ $false )
= $true )).
thf(f3t,axiom,
( ( f3 @ $true )
= $true )).
Petar Vukmirovic
2020-05-29 14:56:22 (GMT)
is a choice symbol.
This problem can become a nigthmare to prove if two conditions are not fulfilled
1) you do not have AVATAR (Lite)
2) you are not careful about the way you deal with booleans
Petar Vukmirovic
2020-05-29 15:0:55 (GMT)
The second part is important for our FBOOL/HOL papers because preprocessing does it better:
Namely preprocessing does the hoisting locally -- that is every disjunct will be transofrmed by inspecting value of the nested boolean resulting in 16 possible transformations of each disjuct... This is repeated independently for 4 disjunts resulting in 64 fold increase in problem size. Then clausifier will smartly rename the formula to avoid excessive duplication and with AVATAR lite the problem is solved in 4s.
Petar Vukmirovic
2020-05-29 15:2:18 (GMT)
On the other hand, if you apply Cases on non AVATAR-split clause you will create clauses because the hoisting transformation is not local, but applies to the whole clause with 4 disjuncts.
Petar Vukmirovic
2020-05-29 15:5:27 (GMT)
So what we need to do is if we observe that the literal has too many boolean subterms is to make prover do things independently on each literal which can be done in two ways:
1) Use AVATAR (works with splittable clauses)
2) Introduce a fresh symbol for the literal, a clause defining a symbol and unfold only on the newly defined clause.
Petar Vukmirovic
2020-05-29 15:6:9 (GMT)
@Alexander Bentkamp, @Visa , @Sophie I am going to put this behavior in one of the papers,
as a very important note
Petar Vukmirovic
2020-05-29 15:6:40 (GMT)
I just wonder how this affects the order -- new symbol should be smaller than the symbols in the literal that is renamed away?
Jasmin Blanchette
2020-05-29 15:9:6 (GMT)
Smaller sounds good (but wait until the experts confirm this), but make sure you have a safe scheme for introducing small new symbols. It's probably enough if the KBO weight is 1 -- no need to in addition making the precedence low, because then you run into the same issue as with the Skolems (which can be solved using ordinals, as Alex pointed out back then).
Petar Vukmirovic
2020-05-29 15:18:22 (GMT)
The solution for making them small in precedence is already in place there -- new symbol is the smallest w.r.t. normal symbols, but larger than all new symbols
Jasmin Blanchette
2020-05-29 15:43:43 (GMT)
Very good. :) I like the discrimination you make between "normal" symbols and, ah well, less normal ones. ;)
Jasmin Blanchette
2020-05-29 15:46:4 (GMT)
But be aware that if the Boolean term you introduce an abbreviation for consists of new symbols only, that might not be enough. That's where KBO weight should save you -- but with LPO, I don't know.
Of course, there are two aspects to this: completeness and efficiency. For efficiency, I'm sure whatever you're doing makes sense. For completeness, maybe the LPO case above is slightly problematic -- something to keep in mind for the complete mode and for the paper.
Alexander Bentkamp
2020-05-29 16:21:20 (GMT)
Introducing a symbol for the entire literal is problematic. But in this case just introducing a symbol for the left-hand side of each literal would be enough, right?
Petar Vukmirovic
2020-05-29 16:21:33 (GMT)
Indeed.
Alexander Bentkamp
2020-05-29 16:38:3 (GMT)
Yeah, we should probably have a simplification rule that has the exact side conditions necessary for the introduction of abbreviation symbols.
Petar Vukmirovic
2020-05-29 17:0:45 (GMT)
I see two situations in which you want to introduce new symbols: casing and clausification
Simon Cruanes
2020-05-29 17:6:47 (GMT)
does the case of custom extensionality rules fall into one of these categories?
Petar Vukmirovic
2020-05-29 17:57:37 (GMT)
hmm... maybe